Termination w.r.t. Q proof of TRS/nontermin/AG01#4.23.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

quot(0, s(y), s(z)) → 0
quot(s(x), s(y), z) → quot(x, y, z)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
quot(x, 0, s(z)) → s(quot(x, plus(z, s(0)), s(z)))

Q is empty.

↳ QTRS

Q restricted rewrite system:
The TRS R consists of the following rules:

quot(0, s(y), s(z)) → 0
quot(s(x), s(y), z) → quot(x, y, z)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
quot(x, 0, s(z)) → s(quot(x, plus(z, s(0)), s(z)))

Q is empty.